nLab proof theory

Contents

Idea

Proof theory is that part of mathematical logic which is concerned with the notion of formal proof. It was introduced by David Hilbert under the name Beweistheorie as part of Hilbert's program. Since Gödel's incompleteness theorem put an end to the original version of Hilbert’s program, proof theory has broadened its scope to include the following:

Structural proof theory is concerned with the structure of proofs and perspicuous proof calculi for elucidating this structure. This leads to the study of sequent calculi and of natural deduction.
Reductive proof theory is the modern version of Hilbert's program: Instead of hoping to secure all of mathematics with finitistic means, one ask: what rests on what?

That is, one asks for reductions between various formal systems, showing for example that some classical systems can be reduced to constructive systems, or some systems which use a priori impredicative principles can nevertheless be reduced to predicative systems. See also: reverse mathematics.
Ordinal analysis analyzes the provably well-founded recursive ordinals and provably total recursive functions of a theory by devising suitable proof calculi.
Proof mining analyzes proofs of specific statements in order to extract more information than the mere truth of the statement, for instance witnesses or bounds on witnesses of existential statements.

Textbook accounts on proof theory with focus on natural deduction and sequent calculi:

Anne Sjerp Troelstra, Helmut Schwichtenberg, Basic Proof Theory , Cambridge University Press (2000, 2012) [doi:10.1017/CBO9781139168717]
Sara Negri, Jan von Plato, Structural Proof Theory, Cambridge University Press (2010) [doi:10.1017/CBO9780511527340, §1 pdf, §2 pdf]